\chapter{语言设计}
\label{chap:design}

本章是对GSL语言设计的介绍，该语言描述的对象是计算图替换规则，见定义\ref{def:subst_rule}。该语言包含两个主要部分：模式表达式与属性表达式。模式表达式用于表达源子图与目标子图的结构，属性表达式用于表达顶点之间的属性约束关系。本章中将介绍GSL的语法定义、语义定义及其Python API的设计。

\section{语法定义}
\label{sec:syntax}

\subsection{模式表达式}

模式表达式描述的是替换规则$\phi$中源模式图$G_s$与目标模式图$G_t$的结构。由于模式图和计算图具有类似的结构，仅仅是顶点存储的信息不同，所以模式表达式拥有和计算表达式类似的形式。记模式表达式的元变量为$p$，其BNF语法如图\ref{fig:pat_syn}所示。

\begin{figure}[htbp]
    \begin{alignat*}{4}
         & p & \quad & \models     & \quad & *                                                                   & \quad & \text{通配符}       \\
         &   &       & \mathrel{|} &       & \mathtt{Const}\ a                                                   &       & \text{常量模式}     \\
         &   &       & \mathrel{|} &       & \mathtt{Variable} \ \{\mathtt{shape}=a,\mathtt{dtype}=a\}           &       & \text{变量模式} \\
         &   &       & \mathrel{|} &       & \mathtt{Call}\ op\ (p, p, \dots, p)\ \{l_1=a, l_2=a, \dots, l_m=a\} &       & \text{算子调用模式} \\
         &   &       & \mathrel{|} &       & \mathtt{Tuple}\ (p, p, \dots, p)                                    &       & \text{元组构成模式} \\
         &   &       & \mathrel{|} &       & \mathtt{Proj}\ e\ \{\mathtt{index}=a\}                              &       & \text{元组投影模式}
    \end{alignat*}
    \caption{模式表达式的BNF语法}
    \label{fig:pat_syn}
\end{figure}

相比计算表达式，模式表达式新增了通配符$*$用于匹配任意表达式。其余的五种模式表达式在计算表达式中都有对应的形式，为了区分两类表达式，模式表达式（除通配符外）均以特定标识符作为前缀。变量、算子调用和元组投影模式都含有属性表达式字典，表示该模式中的这些属性可以用于建立约束。

类似于计算表达式序列与计算图的双向映射$\mathscr{F}$，模式表达式序列$\mathbf{p}=\langle p_1, p_2, \dots, p_n\rangle$与模式图$G_p$之间也存在双向映射$\mathscr{G}$。其对应关系与\ref{sec:graph}节中介绍的$\mathscr{F}$基本相同，仅仅在处理表达式的形式以及图顶点储存的信息上有所区别，在此不作赘述。由于这种相似性，可以定义关于模式表达式的相等、直接子表达式、子表达式等关系。

对于一条图替换规则$\phi=(G_s, G_t)$，它总可以用源子图与目标子图所对应的模式表达式序列$(\mathbf{p}_s, \mathbf{p}_t)=(\mathscr{G}^{-1}(G_s),\mathscr{G}^{-1}(G_t))$表达。至此，实现了图替换规则与表达式替换规则的互相转化。模式表达式语言，以及由其定义的表达式替换规则，由于形式明确、易于推理，在\ref{sec:sema}节中会使用模式表达式来定义语义规则。而模式图，以及由其定义的图替换，由于其能够直观地表达替换的结构特点，在\ref{sec:bidir_match}节中会使用模式图来描述双向匹配算法。

\subsection{属性表达式}
\label{sec:attr}

要表达一条图替换规则，除了源模式图与目标模式图的结构之外，还有模式图顶点属性的约束。属性约束就是属性值之间的数学关系，形式为$a=a$，其中$a$为属性表达式的元变量。然而一个模式图中的属性约束可能很多，一些计算表达式的属性值可能是元组等复合结构，将这些关系全部用等式逐条地显式表达会比较繁琐。另一种可能的思路就是用隐含的方式，即将一个模式表达式的某个属性用对常量或者其它模式表达式属性值的计算来表达，属性的数学关系便隐含在这一表达式中了，这就是属性表达式与模式表达式的联系。图\ref{fig:attr_syn}给出了属性表达式的BNF语法。

\begin{figure}[htbp]
    \begin{alignat*}{4}
         & a & \quad & \models     & \quad & v                & \quad & \text{常量属性}     \\
         &   &       & \mathrel{|} &       & \mathtt{any}     &       & \text{任意属性}     \\
         &   &       & \mathrel{|} &       & p.l              &       & \text{属性访问}     \\
         &   &       & \mathrel{|} &       & a\ bop\ a        &       & \text{二元属性运算} \\
         &   &       & \mathrel{|} &       & (a, a, \dots, a) &       & \text{元组构成属性} \\
         &   &       & \mathrel{|} &       & a.a              &       & \text{元组投影属性}
    \end{alignat*}
    \caption{属性表达式的BNF语法}
    \label{fig:attr_syn}
\end{figure}

属性表达式具有六种基本形式。常量属性和任意属性都是属性表达式的值。属性访问表示访问模式表达式$p$的名称为$l$的属性值。$a\ bop\ a$表示将二元运算符$bop$两侧的属性值作二元运算。当然也可以支持一元运算，本文为了简化讨论而省略。属性表达式也支持元组的构成和投影，用于构造元组构成的属性值以及访问元组属性的某个元素。

\subsection{可变模式}

目前已经介绍了GSL固定模式的核心语法，已经可以覆盖大部分的图替换规则，但是部分替换规则可能要求可变模式。可变模式图是指进行匹配之前所匹配子图$G_m$的结构没有完全固定，而只知道$G_m$可能是由若干结构相似的分支构成的，这些相似的分支可以用同一个模式图来描述。相应地从模式表达式的角度，也可以定义可变模式表达式。

在GSL中目前支持两类可变模式，一类是元组构成顶点可以有可变多个前驱，或者说元组构成表达式有可变多个字段；另一种是$G_m$的输出顶点序列$\mathbf{v}^o_m$可以为变长，或者说计算表达式序列$\mathbf{e}$可以为变长。如果将$\mathbf{e}$也看作一个元组，则可以将其转化为第一种情况。这说明这两种可变模式是统一的，可以用同一个模式表达式去描述。图\ref{fig:var_pat_syn}对图\ref{fig:pat_syn}所表述的模式表达式语法基础上进行扩展，增加了对于可变模式的定义。

\begin{figure}[htbp]
    \begin{alignat*}{4}
         & p & \quad & \models     & \quad & \dots                                                      & \quad &                 \\
         &   &       & \mathrel{|} &       & \mathtt{Variadic}\ p\ \{p, p, \dots, p\}\ \mathbf{f}\ s\ a &       & \text{可变模式} \\
         &   &       & \mathrel{|} &       & \mathtt{Inst}\ p_V\ p\ a                                   &       & \text{实例访问}
    \end{alignat*}
    \caption{扩展可变模式表达式的BNF语法}
    \label{fig:var_pat_syn}
\end{figure}

可变模式表达式中，$p$表示分支的模式，即单个元组字段的模式或者单个输出表达式的模式。$\{p, p, \dots, p\}$是一个集合，也可以记作$S_t$，它记录了可变模式的模版集合。模版可以是任意模式表达式，在可变模式匹配、改写每一个字段模式$p$时，会为每一个$p_t$满足$p_t\subseteq p\wedge p_t\in S_t$复制一个新的模式表达式，这一过程也称为\emph{实例化}（instantiation），所生成的新模式表达式称为模式实例，同时还会生成从模板到实例的映射$f$。模式表达式实例化的具体算法可见算法\ref{alg:inst_tmpl}，其中$f[p\mapsto p\prime]$表示将模板与实例的对应关系$\langle p, p\prime\rangle$添加到到映射$f$中。$\mathbf{f}=\langle f_1, f_2, \dots, f_n\rangle$，其中$f_i, i\in1..n$表示第$i$次实例化产生的映射。初始定义时$\mathbf{f}$为空，可变模式具体化（定义见下段）后$\mathbf{f}$中才包含元素。

\SetKwFunction{Instantiate}{Instantiate}

\begin{algorithm}[tbp]
    \caption{实例化模式表达式}
    \label{alg:inst_tmpl}

    \KwData{模式表达式$p$，模版表达式集合$S_t$}
    \KwResult{实例化的模式表达式$p\prime$，模版到实例的映射$f$}
    \BlankLine

    \Fn{\Instantiate{$p$}}{
        \eIf{$p\in S_t$}{
            $p\prime\leftarrow$复制$p$的基本形式\;
            \ForEach{$p_i\sqsubset_i p$}{
                $p_i\prime\leftarrow\ $\Instantiate{$p_i$}\;
                将$p_i\prime$填入$p\prime$的相应位置，使$p_i\prime\sqsubset_i p\prime$\;
            }
            $f\leftarrow f[p\mapsto p\prime]$\;
            \textbf{return}\ $p\prime$\;
        }{
            \textbf{return}\ $p$\;
        }
    }
\end{algorithm}

在可变模式参与匹配和改写的过程中，会根据需要进行特定次数的实例化，并将模板-实例的映射存储到$\mathbf{f}$中。此时其长度确定了下来，每次实例化的模板-实例映射也得到了，这一过程称为可变模式的\emph{具体化}（concretization），$\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a \stackrel{C}{\to} \mathtt{Variadic}\ p_f\ S_t\ \langle f_1, f_2, \dots, f_n\rangle\ s\ a$表示将$\stackrel{C}{\to}$左侧的可变模式具体化为右侧的可变模式。注意这一过程中只有$\mathbf{f}$从$\langle \rangle$变化为了$\langle f_1, f_2, \dots, f_n\rangle$，其余均没有变化。

可变模式表达式中的$s$为一符号，指示当前所匹配字段的索引。在改写过程中，$s$会被映射到具体的索引值，使得各个分支的结构在符合$p$的基础上，在表达式属性上可以具有一定差异。$s$实际上也是一个属性表达式，在对属性表达式的扩展中会定义该形式。$a$为该可变模式的长度，该属性只在表达式改写时有效，而在匹配时不会使用。

实例访问提供了通过模版表达式访问其对应某个实例的方法。模式实例是通过实例化算法生成的，而非编写者定义的，而真正用于匹配计算表达式的是模式实例，所以需要一个方式获取模式模板对应的模式实例。其中$p_V$指向初始定义的可变模式表达式，$p$表示待查的模版表达式，$a$为所查找实例索引的属性表达式。$p_V$具体化后，实例访问模式才是有效的。

在扩展模式表达式，使其支持可变模式后，也需要对属性表达式进行扩展，使其配合模式表达式来表达可变模式，其语法可见图\ref{fig:var_attr_syn}。

\begin{figure}[htbp]
    \begin{alignat*}{4}
         & a & \quad & \models     & \quad & \dots                 & \quad &                     \\
         &   &       & \mathrel{|} &       & s                     &       & \text{符号}         \\
         &   &       & \mathrel{|} &       & \mathtt{var}\ a\ s\ a &       & \text{可变元组属性} \\
         &   &       & \mathrel{|} &       & \Sigma \ a\ s\ a      &       & \text{求和属性}
    \end{alignat*}
    \caption{扩展可变模式表达式的BNF语法}
    \label{fig:var_attr_syn}
\end{figure}

新增的属性表达式形式中，符号$s$在之前已作过介绍。可变元组属性可以构造变长字段的元组属性值，第一个$a$表示元组字段的属性模版，$s$表示索引符号，第二个$a$表示元组长度，元组长度只在改写时涉及。求和属性可以对一系列属性的和建立约束，第一个$a$表示求和的一项，$s$表示索引符号，第二个$a$表示所求和元素个数。事实上，所有涉及约简（reduction）的属性运算（如平均值、最大值等）都可以采用和求和属性类似的形式。为了简化讨论，本文只定义了求和这一种运算。

\section{语义定义}
\label{sec:sema}

\ref{sec:syntax}节中给出了GSL的语法定义，介绍模式表达式与属性表达式各形式的含义。这其中包含了一定的对其语义的描述，但这种描述是不够明确的。本节中将通过推理规则的形式给出各表达式准确的语义。首先介绍属性表达式的求值与匹配，随后介绍模式表达式的匹配与改写语义。

\subsection{属性表达式的求值与匹配}

属性表达式表达了属性值的计算方式，属性表达式的求值贯穿于计算图替换的整个过程中。求值语义可以用大步语义（Big-Step Semantics）来描述，即$a\Downarrow v$，表示属性表达式可以$a$最终可以求出值为$v$。但由于属性表达式的可变模式扩展中引入了符号，所以还需要一个从符号到值的映射$\Gamma$，称之为环境。$\{\}$表示空环境，$\Gamma[s\mapsto v]$表示将符号与值的对应关系$\langle s,v\rangle$添加到环境$\Gamma$中。因此，求值语义的判断形式应该为$\Gamma;a\Downarrow v$，表示在环境$\Gamma$下属性表达式$a$求得的值为$v$。图\ref{fig:attr_eval}给出了属性表达式的求值语义。

\begin{figure}[tb]
    \begin{multicols}{2}
        \begin{equation}
            \inferrule{ }{v\Downarrow v}
            \tag{\textsc{AE-Value}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma(s)=v}{\Gamma;s\Downarrow v}
            \tag{\textsc{AE-Symbol}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma\vdash p\simeq e \\ attr(e)(l)=v}{\Gamma;p.l \Downarrow v}
            \tag{\textsc{AE-Access}}
            \label{rule:ae_access}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma;a_1\Downarrow v_1 \\ \Gamma;a_2\Downarrow v_2 \\ bop(v_1, v_2)=v}{\Gamma;a_1\ bop\ a_2 \Downarrow v}
            \tag{\textsc{AE-Binary}}
            \label{rule:ae_binary}
        \end{equation}
        \begin{equation}
            \inferrule{\forall i\in 1..n: \Gamma;a_i\Downarrow v_i}{\Gamma;(a_1, a_2, \dots, a_n)\Downarrow (v_1, v_2, \dots, v_n)}
            \tag{\textsc{AE-Tuple}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma;a_t\Downarrow (v_1, v_2, \dots, v_n) \\ \Gamma;a_p\Downarrow k \\ 1\leq k\leq n}{\Gamma;a_t.a_p\Downarrow v_k}
            \tag{\textsc{AE-Proj}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma;a_l\Downarrow n \\ n\in\mathbb{N}^* \\ \forall i\in 1..n: \Gamma[s\mapsto i];a_f\Downarrow v_i}{\Gamma;\mathtt{var}\ a_f\ s\ a_l \Downarrow (v_1, v_2, \dots, v_n)}
            \tag{\textsc{AE-Var}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma;a_l\Downarrow n \\ n\in\mathbb{N}^* \\ \forall i\in 1..n: \Gamma[s\mapsto i];a_t\Downarrow v_i \\ \sum_{i=1}^n v_i=v}{\Gamma;\Sigma\ a_t\ s\ a_l\Downarrow v}
            \tag{\textsc{AE-Sum}}
        \end{equation}
    \end{multicols}
    \caption{属性表达式的求值语义规则}
    \label{fig:attr_eval}
\end{figure}

规则\ref{rule:ae_access}中$\Gamma\vdash p\simeq e$表示在环境$\Gamma$中可推导出模式表达式$p$匹配计算表达式$e$，模式表达式的具体语义将在\ref{sec:pat_match}节中介绍。规则\ref{rule:ae_binary}中$bop(v_1, v_2)$表示将$v_1,v_2$按照$bop$所表示的二元运算对$v_1$和$v_2$进行求值。其余规则的含义比较明显，在此不作叙述。

在属性表达式中，有时并不能通过比较求得的属性值与计算表达式对应位置属性值是否相等，来判断约束是否成立：\texttt{any}不与任何计算表达式的属性值相等；元组属性可能部分字段为\texttt{any}；可变属性需要根据待匹配的实际属性值来确定其长度。为了处理这几种情况，定义了属性表达式的匹配判断形式$\Gamma\vdash a\cong v$，表示在环境$\Gamma$下属性表达式$a$和计算表达式的属性值$v$匹配。图\ref{fig:attr_match}给出了属性表达式的匹配语义规则。

\begin{figure}[tb]
    \begin{multicols}{2}
        \begin{equation}
            \inferrule{ }{\Gamma;\mathtt{any}\cong v}
            \tag{\textsc{AM-Any}}
        \end{equation}
        \begin{equation}
            \inferrule{\Gamma;a\Downarrow v}{\Gamma;a\cong v}
            \tag{\textsc{AM-Eval}}
        \end{equation}
        \begin{equation}
            \inferrule{\forall i\in 1..n: \Gamma\vdash a_i\cong v_i}{\Gamma\vdash (a_1, a_2, \dots, a_n)\cong(v_1, v_2, \dots, v_n)}
            \tag{\textsc{AM-Tuple}}
        \end{equation}
        \begin{equation}
            \inferrule{\forall i\in 1..n: \Gamma[s\mapsto i]\vdash a_f\cong v_i}{\Gamma\vdash \mathtt{var}\ a_f\ s\ a_l\cong (v_1, v_2, \dots, v_n)}
            \tag{\textsc{AM-Var}}
        \end{equation}
    \end{multicols}
    \caption{属性表达式的匹配语义规则}
    \label{fig:attr_match}
\end{figure}

\subsection{模式表达式的匹配}
\label{sec:pat_match}

模式图与计算图的匹配，或者说模式表达式序列与计算表达式序列的匹配，是替换的第一步。这一步需要匹配计算表达式的结构，并检查属性约束是否满足。考虑到可变模式需要依赖环境，定义模式表达式匹配的判断形式为$\Gamma\vdash p\simeq e$，表示在环境$\Gamma$下模式表达式$p$匹配计算表达式$e$。由于图替换$\tau$中的$f$是双射函数，某一特定环境下$p$和$e$必须也是一一对应的，即$\Gamma\vdash p\simeq e$隐含了对于任意$p\prime\neq p,e\prime\neq e$，$\Gamma\vdash p\prime \simeq e$与$\Gamma\vdash p\simeq e\prime$均不成立。给定一个模式表达式序列$\mathbf{p}=\langle p_1, p_2, \dots, p_n\rangle$，如果能在计算表达式$e$中找到$\mathbf{e}=\langle e_1, e_2, \dots, e_n\rangle$满足$\forall i\in 1..n: e_i\subseteq e \wedge \{\}\vdash p_i\simeq e_i$，则称$\mathbf{p}$与$\mathbf{e}$匹配，或者说模式图$\mathscr{G}(\mathbf{p})$与计算图$\mathscr{F}(\mathbf{e})$匹配。图\ref{fig:pat_match}给出了模式表达式点的匹配语义。

\begin{figure}[tb]
    \begin{equation}
        \inferrule{ }{\Gamma\vdash *\simeq e}
        \tag{\textsc{PM-Wildcard}}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma\vdash a\cong v}{\Gamma\vdash \mathtt{Const}\ a\simeq v}
        \tag{\textsc{PM-Const}}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma\vdash a_s\cong v_s \\ \Gamma\vdash a_d\cong v_d}{\Gamma\vdash \mathtt{Variable}\ \{\mathtt{shape}=a_s, \mathtt{dtype}=a_d\}\simeq x\ \{\mathtt{shape}=v_s, \mathtt{dtype}=v_d\}}
        \tag{\textsc{PM-Variable}}
    \end{equation}
    \begin{equation}
        \inferrule{\forall i\in 1..n: \Gamma\vdash p_i\simeq e_i \\ \forall j\in 1..m: \Gamma\vdash a_j\cong v_j}{\Gamma\vdash \mathtt{Call}\ op\ (p_1, p_2, \dots, p_n)\ \{l_1=a_1, l_2=a_2, \dots, l_m=a_m\}\simeq\\\\ op\ (e_1, e_2, ..., e_n)\ \{l_1=v_1, l_2=v_2, \dots, l_m=v_m\}}
        \tag{\textsc{PM-Call}}
    \end{equation}
    \begin{equation}
        \inferrule{\forall i\in 1..n: \Gamma\vdash p_i\simeq e_i}{\Gamma\vdash \mathtt{Tuple}\ (p_1, p_2, \dots, p_n)\simeq (e_1, e_2, \dots, e_n)}
        \tag{\textsc{PM-Tuple}}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma\vdash p\simeq e \\ \Gamma\vdash a\cong i}{\Gamma\vdash \mathtt{Proj}\ p\ \{\mathtt{index}=a\}\simeq e.i}
        \tag{\textsc{PM-Proj}}
    \end{equation}
    \begin{equation}
        \inferrule{\forall i\in 1..n: \mathtt{Instantiate}(p_f, S_t)=(p_i, f_i)\wedge \Gamma[s\mapsto i]\vdash p_i\simeq e_i}{\Gamma\vdash\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a \simeq (e_1, e_2, \dots, e_n) \\ \mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a \stackrel{C}{\to} \mathtt{Variadic}\ p_f\ S_t\ \langle f_1, f_2, \dots, f_n\rangle\ s\ a}
        \tag{\textsc{PM-Variadic}}
        \label{rule:pm_variadic}
    \end{equation}
    \begin{equation}
        \inferrule{\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a_l \stackrel{C}{\to} \mathtt{Variadic}\ p_f\ S_t\ \langle f_1, f_2, \dots, f_n\rangle\ s\ a_l \\ \Gamma;a\Downarrow i \\ i\in\mathbb{N}^* \\ f_i(p_t)=p_i \\ \Gamma\prime\vdash p_i\simeq e}{\Gamma\vdash \mathtt{Inst}\ (\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a_l)\ p_t\ a \simeq e}
        \tag{\textsc{PM-Inst}}
        \label{rule:pm_inst}
    \end{equation}
    \caption{模式表达式的匹配语义规则}
    \label{fig:pat_match}
\end{figure}

模式表达式和计算表达式形式类似，所以只需要将对应形式的模式表达式与计算表达式进行匹配即可。其基本遵循以下模式：若有子表达式，则检查对应位置子表达式是否匹配；若有属性，则检查对应名称的属性值是否匹配。注意到规则\ref{rule:pm_variadic}中参与匹配的是不包含模板-实例映射的可变模式，这是因为语言编写者定义的可变模式不可能含有这些映射。在具体化后，会通过$\stackrel{C}{\to}$建立原始的可变模式与具体化可变模式的关系。规则\ref{rule:pm_inst}指向不含映射的可变模式也是相同的原因。由于具体化过程会建立原始可变模式与具体化可变模式的关系，所以可以找到模板-实例映射，从而找到某个模板对应的某个实例。

\subsection{模式表达式的改写}

通过目标模式图生成替换后的计算图，或者说从目标模式表达式生成替换后的计算表达式，是替换的第二步。这一步的工作就是作一个从模式表达式到计算表达式的映射，然后再将原计算表达式中对应位置的子表达式置换。置换是非常容易的，此处仅讨论映射的语义。定义模式表达式映射的判断形式为$\Gamma;p\mapsto e$，表示在环境$\Gamma$下从模式表达式$p$可以映射到计算表达式$e$。给定模式表达式序列$\mathbf{p}=\langle p_1, p_2, \dots, p_n\rangle$，一定存在计算表达式序列$\mathbf{e}=\langle e_1, e_2, \dots, e_n\rangle$，满足$\forall i\in 1..n: \{\};p_i\mapsto e_i$，则称$\mathbf{p}$可映射到$\mathbf{e}$，或者说模式图$\mathscr{G}(\mathbf{p})$可映射到$\mathscr{F}(\mathbf{e})$。模式表达式的映射语义可见图\ref{fig:pat_map}。

\begin{figure}[tb]
    \begin{equation}
        \inferrule{\Gamma\vdash p\simeq e}{\Gamma\prime;p\mapsto e}
        \tag{\textsc{PE-Match}}
        \label{rule:pe_match}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma;a\Downarrow v}{\Gamma;\mathtt{Const}\ a\mapsto v}
        \tag{\textsc{PE-Const}}
    \end{equation}
    \begin{equation}
        \inferrule{\forall i\in 1..n: \Gamma;p_i\mapsto e_i \\ \forall j\in 1..m: \Gamma;a_j\Downarrow v_j}{\Gamma;\mathtt{Call}\ op\ (p_1, p_2, \dots, p_n)\ \{l_1=a_1, l_2=a_2, \dots, l_m=a_m\} \mapsto\\\\ op\ (e_1, e_2, ..., e_n)\ \{l_1=v_1, l_2=v_2, \dots, l_m=v_m\}}
        \tag{\textsc{PE-Call}}
    \end{equation}
    \begin{equation}
        \inferrule{\forall i\in 1..n: \Gamma;p_i\mapsto e_i}{\Gamma;\mathtt{Tuple}\ (p_1, p_2, \dots, p_n)\mapsto (e_1, e_2, \dots, e_n)}
        \tag{\textsc{PE-Tuple}}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma;p\mapsto e \\ \Gamma;a\Downarrow i}{\Gamma;\mathtt{Proj}\ p\ \{\mathtt{index}=a\}\mapsto e.i}
        \tag{\textsc{PE-Proj}}
    \end{equation}
    \begin{equation}
        \inferrule{\Gamma;a\Downarrow n \\ n\in\mathbb{N}^* \\ \forall i\in 1..n: \mathtt{Instantiate}(p_f, S_t)=(p_i, f_i)\wedge \Gamma[s\mapsto i];p_i\mapsto e_i}{\Gamma;\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a \mapsto (e_1, e_2, \dots, e_n) \\ \mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a \stackrel{C}{\to} \mathtt{Variadic}\ p_f\ S_t\ \langle f_1, f_2, \dots, f_n\rangle\ s\ a}
        \tag{\textsc{PE-Variadic}}
        \label{rule:pe_variadic}
    \end{equation}
    \begin{equation}
        \inferrule{\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a_l \stackrel{C}{\to} \mathtt{Variadic}\ p_f\ S_t\ \langle f_1, f_2, \dots, f_n\rangle\ s\ a_l \\ \Gamma;a\Downarrow i \\ i\in\mathbb{N}^* \\ f_i(p_t)=p_i \\ \Gamma\prime;p_i\mapsto e}{\Gamma;\mathtt{Inst}\ (\mathtt{Variadic}\ p_f\ S_t\ \langle\rangle\ s\ a_l)\ p_t\ a \mapsto e}
        \tag{\textsc{PE-Inst}}
    \end{equation}
    \caption{模式表达式的映射语义规则}
    \label{fig:pat_map}
\end{figure}

规则\ref{rule:pe_match}描述了已匹配的计算表达式可以作为新的计算表达式的一部分，这是目标计算表达式的一个来源。其余的规则描述了如何通过模式表达式构造新的计算表达式，这是目标计算表达式的另一个来源。其形式和图\ref{fig:pat_match}中描述的匹配规则较为相似。注意可变模式\ref{rule:pe_variadic}中需要先求出长度再进行具体化。同时注意映射语义不包含从通配符或变量模式创建新计算表达式的规则，因为它们属于输入表达式，目标计算表达式不可能包含源计算表达式中没有的输入子表达式。

至此已经介绍完了GSL所有的语义规则。可以发现，无论是属性表达式的求值与匹配，还是模式表达式的匹配和改写，都仅仅只是逻辑上的定义，并没有规定其具体的运行模式，这说明GSL是一种声明式的语言。正因如此，才能使语言的使用者关注图替换的结构本质，不需要去关心具体的算法细节。在\ref{chap:impl}章中会给出该语言的一种可能的实现，其运行方式基本能够符合本节规定的语义。

\section{Python API设计}

Python语言具有简洁、灵活、互操作性强等特点，在深度学习编程中起到了关键性的作用，为此GSL被设计为一门嵌入Python的领域特定语言，利用Python自身的特性简化编程。编写GSL程序是通过调用语言提供的应用程序编程接口（Application Programming Interface, API）来完成的，所以API设计也是语言设计的一部分。本节主要阐述如何将GSL的语法用Python语言进行表示。

在GSL中，需要向用户提供的接口有下列三类：模式表达式，用于定义源子图和目标子图的结构；属性表达式，用于表达属性约束；以及替换规则，将模式表达式和属性表达式定义的模式组装成一个完整的替换规则。所有表达式都用类进行定义，用户通过调用API构造对应表达式的抽象语法树（Abstract Syntax Tree，AST）。在设计类的具体方法时，尽可能地利用Python自身的语言特性与作用域规则，最大程度地简化语言的编写。

\begin{figure}[htbp]
    \begin{lstlisting}
from gsl import pat, attr, op, Subst

# 创建工作负载
wl = ...  # 具体代码已省略

# 输入
x = pat.Wildcard()
w1 = pat.Variable()
w = pat.Variable(shape=(None, None, w1.shape[2], w1.shape[3]))

# 源模式
conv1 = op.Conv2D(x, w1, groups=1)
conv_attrs = ['strides', 'padding', 'dilation', 'groups']
conv = op.Conv2D(x, w, **pat.same_attr(conv1, conv_attrs))
src = pat.Variadic(conv, templates=[conv, w], first=[conv1, w1], min_len=2)

# 目标模式
i = attr.Symbol()
w_inst = src(w, i)
concat = op.Concatenate(pat.Variadic(w_inst, templates=[w_inst], index=i, length=src.length), axis=0)
conv = op.Conv2D(x, concat, **pat.same_attr(conv1, conv_attrs))
split = op.Split(conv, axis=1, indices_or_sections=attr.Variadic(lambda j: attr.ReduceIndexed(attr.BinaryOp.ADD, lambda k: src(w, k).shape[0], j + 1), length=src.length - 1))
i = attr.Symbol()
item = split[i]
tgt = pat.Variadic(item, templates=[item], index=i)

# 创建替换规则
subst = Subst(src, tgt)

# 将替换作用于工作负载
new_wl = subst(wl)
\end{lstlisting}
    \caption{GSL并行卷积合并规则示例代码}
    \label{fig:code_sample}
\end{figure}

模式表达式的定义方式如下：每构造一个模式表达式对象，就可以绑定到一个Python的局部变量上，以便在后续模式表达式的构造中被多次使用；如果一个模式表达式仅被使用一次，也可以嵌套在其它模式表达式的构造函数调用中。模式表达式对象的引用关系能构成一张有向无环图，和模式图的结构一致。这和使用主流深度学习框架如TensorFlow\cite{abadi2016tf}、PyTorch\cite{paszke2019pytorch}等API定义模型的方式是相同的。此外，可以通过一系列手段简化模式表达式的编写。第一，可以重载模式表达式类的运算符，如重载四则运算符以简洁地表达四则运算模式、重载\texttt{\_\_getitem\_\_}方法以表达元组投影模式等；第二，可以为每个算子单独创建一个算子调用模式的子类，在其构造函数参数中明确标出所需的输入参数和属性，以提供更好的提示。

属性表达式是在模式表达式构造函数的关键词参数（keyword argument）中定义的，正好符合语法定义中的$l=a$的形式。在属性表达式的各种形式中，属性访问是通过重载模式表达式类的\texttt{\_\_getattr\_\_}方法表达的，四则运算与元组投影也重载了对应的运算符。属性表达式也可以绑定到变量上，以实现不同属性表达式之间公共子表达式的复用。

替换规则的定义则更为简单，只需要源模式表达式序列和目标模式表达式序列直接传入即可。替换规则类重载了\texttt{\_\_call\_\_}方法，可以直接以函数调用的形式作用于某个工作负载，返回新的工作负载，这样使得执行替换只需要一行代码就可以完成。

图\ref{fig:code_sample}展示了使用GSL的Python API编写一条规则并作用于某工作负载，该规则可以将对同一数据所进行的若干并行卷积合并为一个单独的卷积。该规则展示了一个GSL程序的基本结构，以及其对于可变模式的支持。该程序仅仅用于展示Python API的大致特点，其具体的程序逻辑并非本节的重点，故不对其展开讲解。

\section{本章小结}

本章主要介绍了GSL的语言设计，包括语法定义、语义定义与Python API设计。首先，给出了模式表达式与属性表达式的语法，然后对其进行了扩充以支持可变模式。然后，给出了属性表达式的求值与匹配语义，以及模式表达式的匹配与改写语义。最后，讨论了GSL作为一门嵌入Python的语言的API设计思想，并给出了相关实例代码。